// ==++==
// 
//   Copyright (c) Microsoft Corporation.  All rights reserved.
// 
// ==--==

using System;
using System.Collections.Generic;
using System.Text;
using Microsoft.ExtendedReflection.Interpretation;
using Microsoft.ExtendedReflection.Metadata;
using Microsoft.ExtendedReflection.Collections;
using System.IO;
using Microsoft.ExtendedReflection.Utilities.Safe.IO;
using Microsoft.ExtendedReflection.Emit;
using Microsoft.ExtendedReflection.Emit.CSharp;
using Microsoft.Pex.Engine.Logging;
using Microsoft.ExtendedReflection.Utilities;
using Microsoft.ExtendedReflection.Interpretation.Visitors;
using Microsoft.ExtendedReflection.Utilities.Safe.Diagnostics;
using Microsoft.ExtendedReflection.Utilities.Safe;
using Microsoft.Pex.Engine;
using Microsoft.Pex.Engine.ComponentModel;
using Microsoft.ExtendedReflection.ComponentModel;

namespace DySy.Engine
{
    /// <summary>
    /// Second main DySy class
    /// </summary>
    internal sealed class DySyManager
        : PexExplorationComponentBase
        , IService
    {
        IDySyOptions _options;

        /// <summary>
        /// Constructor
        /// </summary>
        public DySyManager(IDySyOptions options)
        {
            this._options = options;
        }

        public IDySyOptions Options
        {
            get { return this._options; }
        }

        #region private types        
        /// <summary>
        /// Result value.
        /// Method return value or field value in method post state.
        /// </summary>
        struct Result
        {
            public Term Value;
            public bool HasValue;
            public Term Index;
            public Term IndexedValue;
            public bool HasIndexedValue;
        }

        /// <summary>
        /// State at end of a traversed execution path: 
        /// Method return value and field values
        /// </summary>
        /// <remarks>
        /// TODO: Add effect the method had on parameter values
        /// </remarks>
        class PathResult
        {
            public Result Return;
            public SafeDictionary<Field, Result> FieldResults = new SafeDictionary<Field, Result>();
        }
        #endregion

        #region private fields
        TermManager termManager;
        TermEmitter emitter;

        /* Traversed method execution paths, by method:
          precondition = path condition --> post condition = method return value and field updates */
        SafeDictionary<Method, SafeDictionary<Term, PathResult>> paths = new SafeDictionary<Method, SafeDictionary<Term, PathResult>>();
        TermSimplifier simplifier;
        SafeDictionary<TypeEx, SafeBag<Term>> potentialInvariants = new SafeDictionary<TypeEx, SafeBag<Term>>();
        SafeDictionary<TypeEx, SafeSet<Term>> invariants = new SafeDictionary<TypeEx, SafeSet<Term>>();
        SafeSet<MethodDefinition> impureMethods = new SafeSet<MethodDefinition>();
        #endregion

        protected override void Initialize()
        {
            this.termManager = this.ExplorationServices.TermManager;
            this.emitter = new TermEmitter(
                 this.termManager,
                 new NameCreator());
            this.simplifier = new TermSimplifier(this.termManager, true);
        }

        public override void Dispose()
        {
            if (this.simplifier != null)
            {
                this.simplifier.Dispose();
                this.simplifier = null;
            }
            base.Dispose();
        }

        public void SetInvariants(TypeEx declaringType, IEnumerable<Term> invariants)
        {
            this.invariants.Add(declaringType, new SafeSet<Term>(invariants));
        }

        public void AddPotentialInvariant(TypeEx declaringType, Term condition)
        {
            using (SomeRewriter someRewriter = new SomeRewriter(this.termManager))
            {
                condition = someRewriter.VisitTerm(default(TVoid), condition);
                SafeBag<Term> potentialInvariants;
                if (!this.potentialInvariants.TryGetValue(declaringType, out potentialInvariants))
                    this.potentialInvariants[declaringType] = potentialInvariants = new SafeBag<Term>();
                potentialInvariants.Add(condition);
            }
        }

        public IIndexable<TypeEx> GetTypes()
        {
            return Indexable.Enumerable(this.potentialInvariants.Keys);
        }

        public IEnumerable<Term> GetPotentialInvariants(TypeEx type)
        {
            SafeBag<Term> potentialInvariants;
            if (this.potentialInvariants.TryGetValue(type, out potentialInvariants))
                return potentialInvariants.UniqueItems;
            else
                return Indexable.Empty<Term>();
        }

        private PathResult getAddPathResult(Method method, Term pathCondition)
        {
            SafeDictionary<Term, PathResult> methodPaths;
            if (!this.paths.TryGetValue(method, out methodPaths))
                this.paths[method] = methodPaths = new SafeDictionary<Term, PathResult>();

            PathResult res;
            if (!methodPaths.TryGetValue(pathCondition, out res))
                methodPaths[pathCondition] = res = new PathResult();
            return res;
        }

        /// <summary>
        /// Initialize path induced by pathCondition, if not yet initialized.
        /// </summary>
        /// <param name="pathCondition">pre condition</param>
        public void AddPath(Method method, Term pathCondition)
        {
            using (SomeRewriter someRewriter = new SomeRewriter(this.termManager))
            {
                pathCondition = someRewriter.VisitTerm(default(TVoid), pathCondition);
                PathResult p = this.getAddPathResult(method, pathCondition);
            }
        }

        /// <summary>
        /// Set results of path.
        /// Initialize path induced by pathCondition, if not yet initialized.
        /// </summary>
        /// <param name="pathCondition">pre condition</param>
        public void AddPath(Method method, Term pathCondition, Field field, Term[] indices, Term result)
        {
            using (SomeRewriter someRewriter = new SomeRewriter(this.termManager))
            {
                pathCondition = someRewriter.VisitTerm(default(TVoid), pathCondition);
                result = someRewriter.VisitTerm(default(TVoid), result);

                PathResult p = this.getAddPathResult(method, pathCondition);
                Result r;
                if (field == null)
                    r = p.Return;
                else if (!p.FieldResults.TryGetValue(field, out r))
                    r = new Result();
                if (indices.Length == 0)
                {
                    r.HasValue = true;
                    r.Value = result;
                }
                else if (indices.Length == 1)
                {
                    r.HasIndexedValue = true;
                    r.Index = indices[0];
                    r.IndexedValue = result;
                }
                // else TODO
                if (field == null)
                    p.Return = r;
                else
                    p.FieldResults[field] = r;
            }
        }


        #region private classes
        class SomeId : IObjectId
        {
            int index;

            public SomeId(int index)
            {
                this.index = index;
            }

            public override bool Equals(object obj)
            {
                SomeId someId = obj as SomeId;
                return someId != null && someId.index == this.index;
            }

            public override int GetHashCode()
            {
                return this.index;
            }

            #region IObjectId Members

            public string Description
            {
                get { return "some." + this.index.ToString(); }
            }

            public bool TrackFieldAccesses
            {
                get { return false; }
            }

            public ObjectCreationTime CreationTime
            {
                get { return ObjectCreationTime.Unknown; }
            }

            public bool IsFullyDefined
            {
                get { return false; }
            }

            public Int64 GetPersistentHashCode()
            {
                return 0; // TODO
            }
            #endregion
        }

        class SomeRewriter : TermInternalizingRewriter<TVoid>
        {
            SafeBag<TypeEx> types = new SafeBag<TypeEx>();
            public SomeRewriter(TermManager termManager)
                : base(termManager, OnCollection.Fail)
            {
            }

            public override Term VisitObject(TVoid parameter, Term term, IObjectId id, ObjectPropertyCollection properties)
            {
                object value;
                if (this.TermManager.TryGetObject(term, out value))
                    return base.VisitObject(parameter, term, id, properties);
                else
                {
                    TypeEx type;
                    if (!this.TermManager.TryGetObjectType(term, out type))
                        SafeDebug.Fail("cannet get object type");
                    int index = types.Add(type);
                    return this.TermManager.Object(new SomeId(index), properties);
                }
            }

            public override Term VisitSelect(TVoid parameter, Term term, Term compound, Term index)
            {
                index = this.VisitTerm(parameter, index);
                compound = this.VisitTerm(parameter, compound);

                ISymbolId key;
                if (this.TermManager.TryGetSymbol(index, out key))
                {
                    ISymbolIdFromParameter parameterKey = key as ISymbolIdFromParameter;
                    if (parameterKey != null &&
                        parameterKey.Parameter.IsThis)
                    {
                        Term baseCompound;
                        ITermMap updates;
                        if (this.TermManager.TryGetUpdate(compound, out baseCompound, out updates) &&
                            updates.AreKeysValues)
                            return this.VisitTerm(
                                parameter,
                                this.TermManager.Select(baseCompound, index));
                    }
                }

                return this.TermManager.Select(compound, index);
            }
        }

        class InvariantSimplifier : TermInternalizingRewriter<TVoid>
        {
            // TODO: Use equality graph, or even theorem prover for this

            SafeDictionary<Term, bool> invariants = new SafeDictionary<Term, bool>();
            public InvariantSimplifier(
                TermManager termManager,
                IEnumerable<Term> invariants)
                : base(termManager, OnCollection.Fail)
            {
                foreach (var invariant in invariants)
                {
                    this.invariants[invariant] = true;
                    this.invariants[termManager.LogicalNot(invariant)] = false;
                }
            }

            public override Term VisitTerm(TVoid parameter, Term term)
            {
                bool res;
                if (this.invariants.TryGetValue(term, out res))
                    return this.TermManager.I4(res);
                else
                    return base.VisitTerm(parameter, term);
            }
        }

        class UniqueSubtermCounter : TermInternalizingRewriter<TVoid>
        {
            public UniqueSubtermCounter(TermManager termManager)
                : base(termManager, OnCollection.Fail)
            {
            }
        }
        #endregion

        /// <summary>
        /// Second main entry into DySy
        /// Called at end to dump collected data.
        /// </summary>
        public void Dump()
        {
            // group methods by types
            SafeDictionary<TypeEx, SafeSet<Method>> grouped = new SafeDictionary<TypeEx, SafeSet<Method>>();
            foreach (var method in this.paths.Keys)
            {
                TypeEx dt;
                if (method.TryGetDeclaringType(out dt))
                {
                    SafeSet<Method> methods;
                    if (!grouped.TryGetValue(dt, out methods))
                        grouped[dt] = methods = new SafeSet<Method>();
                    methods.Add(method);
                }
            }

            SafeSet<Term> globalSubterms = new SafeSet<Term>();
            SafeBag<TypeEx> typeSubtermsCounts = new SafeBag<TypeEx>();
            SafeBag<Method> methodSubtermsCounts = new SafeBag<Method>();
            foreach (SafeKeyValuePair<TypeEx, SafeSet<Method>> kvp in grouped)
            {
                int typeItems;
                SafeSet<Term> typeSubterms = new SafeSet<Term>();
                SafeSet<Term> invariants;
                string invariantsText;
                try
                {
                    invariantsText = this.getInvariantsText(typeSubterms, kvp, out invariants, out typeItems);
                }
                catch (OutOfMemoryException)
                {
                    invariantsText = "OutOfMemoryException";
                    invariants = new SafeSet<Term>();
                    typeItems = 0;
                }
                try
                {
                    this.Log.Dump(
                        DySyLogCategories.DySy,
                        SafeString.Format(
                            "invariants of {0}",
                            kvp.Key.FullName),
                            invariantsText);
                }
                catch (OutOfMemoryException)
                {
                }

                using (InvariantSimplifier invariantSimplifier = new InvariantSimplifier(this.termManager, invariants))
                {
                    foreach (var m in kvp.Value)
                    {
                        SafeSet<Term> methodSubterms = new SafeSet<Term>();
                        string preAndPostConditionsText;
                        int items;
                        try
                        {
                            preAndPostConditionsText = this.getPreAndPostConditionsText(methodSubterms, invariantSimplifier, kvp.Key, m, out items);
                        }
                        catch (OutOfMemoryException)
                        {
                            preAndPostConditionsText = "OutOfMemoryException";
                            items = 0;
                        }
                        try
                        {
                            this.Log.Dump(
                                DySyLogCategories.DySy,
                                SafeString.Format(
                                    "  inferred spec of {0}",
                                    m.SerializableName.ShortTypedNameWithParameters),
                                    preAndPostConditionsText);
                        }
                        catch (OutOfMemoryException)
                        {
                        }

                        typeSubterms.AddRange(methodSubterms);
                        methodSubtermsCounts[m] = methodSubterms.Count + items;
                        typeItems += items;
                    }
                }

                globalSubterms.AddRange(typeSubterms);
                typeSubtermsCounts[kvp.Key] = typeSubterms.Count + typeItems;
            }

            string statisticsString;
            try
            {
                statisticsString = this.getStatisticsText(globalSubterms.Count, typeSubtermsCounts, methodSubtermsCounts);
            }
            catch (OutOfMemoryException)
            {
                statisticsString = "OutOfMemoryException";
            }

            this.Log.Dump(
                DySyLogCategories.DySy,
                "statistics",
                statisticsString);
        }

        private string getStatisticsText(int globalSubtermsCount, SafeBag<TypeEx> typeSubtermsCounts, SafeBag<Method> methodSubtermsCounts)
        {
            SafeStringWriter stringWriter = new SafeStringWriter();
            stringWriter.WriteLine("=== unique subterm counts");
            stringWriter.WriteLine("total: {0}", globalSubtermsCount);
            stringWriter.WriteLine("per types (including invariants and pre/post conditions of their methods)");
            SafeSortedDictionary<string, bool> sorted = new SafeSortedDictionary<string, bool>();
            foreach (SafeKeyValuePair<TypeEx, int> kvp in typeSubtermsCounts)
                sorted[SafeString.Format("  {0}: {1}", kvp.Key, kvp.Value)] = true;
            foreach (var s in sorted.Keys)
                stringWriter.WriteLine(s);
            stringWriter.WriteLine("per method (pre/post conditions)");
            sorted.Clear();
            foreach (SafeKeyValuePair<Method, int> kvp in methodSubtermsCounts)
                sorted[SafeString.Format("  {0}: {1}", kvp.Key, kvp.Value)] = true;
            foreach (var s in sorted.Keys)
                stringWriter.WriteLine(s);
            return stringWriter.ToString();
        }

        /// <summary>
        /// getPreAndPostConditionsText
        /// </summary>
        private string getPreAndPostConditionsText(SafeSet<Term> subterms, InvariantSimplifier invariantSimplifier, TypeEx t, Method m, out int items)
        {
            using (UniqueSubtermCounter usc = new UniqueSubtermCounter(this.termManager))
            {
                SafeDictionary<Term, PathResult> methodPaths = this.paths[m]; // pre condition = path condition --> post condition
                Term disjunction = this.termManager.False;
                foreach (var disjunct in methodPaths.Keys)
                    disjunction = this.termManager.LogicalOr(disjunct, disjunction);
                disjunction = this.simplifier.VisitTerm(default(TVoid), disjunction);
                disjunction = invariantSimplifier.VisitTerm(default(TVoid), disjunction);

                items = 0;
                // pretty print
                SafeStringWriter stringWriter = new SafeStringWriter();
                stringWriter.WriteLine("=== Purity");
                if (!this.impureMethods.Contains(m.Definition))
                {
                    stringWriter.WriteLine("pure; // on all observed paths");
                    items++;
                }

                if (!this.termManager.IsTrue(disjunction))
                {
                    stringWriter.WriteLine("=== Precondition");
                    items++;
                    this.dump(usc, stringWriter, disjunction, SystemTypes.Bool);
                    stringWriter.WriteLine();
                }

                if (this.Options.Compact)
                    stringWriter.WriteLine("=== Postconditions");
                dumpResults(invariantSimplifier, t, m, ref items, usc, methodPaths, disjunction, stringWriter, false);
                dumpResults(invariantSimplifier, t, m, ref items, usc, methodPaths, disjunction, stringWriter, true);

                subterms.AddRange(usc.InternalizedKeys);
                return stringWriter.ToString();
            }
            /*
            stringWriter = new SafeStringWriter();
            SExpWriter writer = new SExpWriter(this.termManager, stringWriter, true, false);
            writer.Write(disjunction);
            writer.WriteLine();
            this.Log.Dump("DaikonSharpRaw", m.FullName, stringWriter.ToString());
            */
        }


        /// <remarks>
        /// TODO: Generalize from fields declared by method's declaring type to
        /// all visible fields (declared by any class).
        /// TODO: Include effect on method parameters.
        /// </remarks>
        private void dumpResults(
            InvariantSimplifier invariantSimplifier, 
            TypeEx t, 
            Method m, 
            ref int items, 
            UniqueSubtermCounter usc, 
            SafeDictionary<Term, PathResult> methodPaths, 
            Term disjunction, 
            SafeStringWriter stringWriter, 
            bool indexed)
        {
            this.dumpResult(usc, invariantSimplifier, disjunction, t, m, null, methodPaths, stringWriter, indexed);
            if (this.impureMethods.Contains(m.Definition))
            {
                TypeEx declaringType;
                if (m.TryGetDeclaringType(out declaringType))
                {
                    foreach (var f in declaringType.DeclaredStaticFields)
                        if (indexed || !f.IsInitOnly && f.Definition.Literal == null)
                        {
                            items++;
                            this.dumpResult(usc, invariantSimplifier, disjunction, t, m, f, methodPaths, stringWriter, indexed);
                        }
                    foreach (var f in declaringType.InstanceFields)
                        if (indexed || m.IsConstructor || !f.IsInitOnly)
                        {
                            this.dumpResult(usc, invariantSimplifier, disjunction, t, m, f, methodPaths, stringWriter, indexed);
                            items++;
                        }
                }
            }
        }

        private string getInvariantsText(SafeSet<Term> subterms, SafeKeyValuePair<TypeEx, SafeSet<Method>> kvp, out SafeSet<Term> invariants, out int items)
        {
            using (UniqueSubtermCounter usc = new UniqueSubtermCounter(this.termManager))
            {
                SafeStringWriter stringWriter = new SafeStringWriter();
                stringWriter.WriteLine("=== Invariants for {0}", kvp.Key.FullName);

                items = 0;
                if (this.invariants.TryGetValue(kvp.Key, out invariants))
                    foreach (var rawCondition in invariants)
                    {
                        Term condition = this.simplifier.VisitTerm(default(TVoid), rawCondition);
                        if (!this.termManager.IsTrue(condition))
                        {
                            items++;
                            stringWriter.WriteLine("------");
                            this.dump(usc, stringWriter, condition, SystemTypes.Bool);
                        }
                    }
                else
                    invariants = new SafeSet<Term>();

                stringWriter.WriteLine();
                stringWriter.WriteLine("=== Potential Invariants for {0} (does not count towards statistics)", kvp.Key.FullName);
                SafeBag<Term> potentialInvariants;
                if (this.potentialInvariants.TryGetValue(kvp.Key, out potentialInvariants))
                    foreach (SafeKeyValuePair<Term, int> kvp2 in potentialInvariants)
                    {
                        Term condition = this.simplifier.VisitTerm(default(TVoid), kvp2.Key);
                        stringWriter.WriteLine("------ Observed {0} times", kvp2.Value);
                        this.dump(null, stringWriter, condition, SystemTypes.Bool);
                        /*
                        SExpWriter writer = new SExpWriter(this.termManager, stringWriter, true, false);
                        writer.Write(condition);
                        writer.WriteLine();
                        */
                    }

                subterms.AddRange(usc.InternalizedKeys);
                return stringWriter.ToString();
            }
        }


        #region private classes
        class PostStateFieldId : ISymbolIdWithType
        {
            Field field;
            bool indexed;
            public PostStateFieldId(Field field, bool indexed)
            {
                this.field = field;
                this.indexed = indexed;
            }

            public override bool Equals(object obj)
            {
                PostStateFieldId other = obj as PostStateFieldId;
                return other != null && this.field == other.field && this.indexed == other.indexed;
            }

            public override int GetHashCode()
            {
                return this.field.GetHashCode();
            }

            #region ISymbolId Members

            public string Description
            {
                get
                {
                    if (indexed)
                        return "(" + field.ShortName + "[$x])" + "'";
                    else
                        return field.ShortName + "'";
                }
            }

            public TypeEx Type
            {
                get
                {
                    if (indexed)
                        return this.field.Type.ElementType;
                    else
                        return this.field.Type;
                }
            }

            public Layout Layout
            {
                get { return this.Type.Layout; }
            }

            public ObjectCreationTime ObjectCreationTime
            {
                get { return ObjectCreationTime.Unknown; }
            }

            public Int64 GetPersistentHashCode()
            {
                return 0; // TODO
            }
            #endregion
        }

        class PostStateResultId : ISymbolIdWithType
        {
            TypeEx type;
            bool indexed;
            public PostStateResultId(TypeEx type, bool indexed)
            {
                this.type = type;
                this.indexed = indexed;
            }

            public override bool Equals(object obj)
            {
                PostStateResultId other = obj as PostStateResultId;
                return other != null && this.type == other.type && this.indexed == other.indexed;
            }

            public override int GetHashCode()
            {
                return this.type.GetHashCode();
            }

            #region ISymbolId Members

            public string Description
            {
                get
                {
                    if (indexed)
                        return "result[$x]";
                    else
                        return "result";
                }
            }

            public TypeEx Type
            {
                get
                {
                    if (indexed)
                        return this.type.ElementType;
                    else
                        return this.type;
                }
            }

            public Layout Layout
            {
                get { return this.Type.Layout; }
            }

            public ObjectCreationTime ObjectCreationTime
            {
                get { return ObjectCreationTime.Unknown; }
            }

            public Int64 GetPersistentHashCode()
            {
                return 0; // TODO
            }
            #endregion
        }
        #endregion


        private void dumpResult(
            UniqueSubtermCounter subterms, 
            InvariantSimplifier invariantSimplifier, 
            Term precondition, 
            TypeEx t, 
            Method m, 
            Field f, 
            SafeDictionary<Term, PathResult> methodPaths, 
            SafeStringWriter stringWriter, 
            bool indexed)
        {
            SafeDictionary<Term, Term> results = getRawPostCondition(f, methodPaths, indexed);

            if (results.Count > 0)
            {
                if (this.Options.Compact)
                {
                    ISymbolIdWithType key;
                    if (f == null)
                        key = new PostStateResultId(m.ResultType, indexed);
                    else
                        key = new PostStateFieldId(f, indexed);
                    Term resultName = this.termManager.Symbol(key);

                    Term res = default(Term);
                    bool first = true;
                    foreach (SafeKeyValuePair<Term, Term> kvp2 in results)
                    {
                        if (first)
                        {
                            first = false;
                            res = kvp2.Key;
                        }
                        else
                            res = this.termManager.IfThenElse(
                                kvp2.Value,
                                kvp2.Key,
                                res);
                    }
                    if (this.termManager.GetLayout(res) != key.Layout)
                        res = this.termManager.Narrow(res, key.Type.Layout.MemoryNarrowing);
                    if (this.termManager.GetLayout(res) != key.Layout)
                        return; // shouldn't happen
                    res =
                        this.termManager.Equality(
                            resultName,
                            res);

                    this.dump(subterms, stringWriter, this.termManager.True, res, SystemTypes.Bool);
                }
                else
                {
                    stringWriter.WriteLine("=== Result {0}{1}",
                        f == null ? "" : f.IsStatic ? f.ShortName : "this." + f.ShortName,
                        indexed ? "[$x]" : "");
                    foreach (SafeKeyValuePair<Term, Term> kvp2 in results)
                    {
                        Term condition = kvp2.Value;
                        condition = this.simplifier.VisitTerm(default(TVoid), condition);
                        condition = invariantSimplifier.VisitTerm(default(TVoid), condition);

                        this.dump(subterms, stringWriter, condition, kvp2.Key, f == null ? m.ResultType : f.Type);
                    }
                }
            }
        }

        /// <summary>
        /// Extract result terms
        /// </summary>
        /// <returns>post condition --> pre condition = (pc1 || pc2 || .. || pcN)</returns>
        private SafeDictionary<Term, Term> getRawPostCondition(
            Field field, 
            SafeDictionary<Term, PathResult> methodPaths, 
            bool indexed)
        {
            SafeDictionary<Term, Term> resultTerms = new SafeDictionary<Term, Term>();
            foreach (SafeKeyValuePair<Term, PathResult> path in methodPaths)
            {
                PathResult pathResult = path.Value;
                Result result;
                if (field == null)  // method return value
                    result = pathResult.Return;
                else if (!pathResult.FieldResults.TryGetValue(field, out result))  // field post state
                    continue;

                Term resultTerm;
                if (indexed)
                    if (result.HasIndexedValue)
                        resultTerm = result.IndexedValue;
                    else
                        continue;
                else
                    if (result.HasValue)
                        resultTerm = result.Value;
                    else
                        continue;

                Term condition;
                if (!resultTerms.TryGetValue(resultTerm, out condition))
                    resultTerms[resultTerm] = condition = this.termManager.False;
                condition = this.termManager.LogicalOr(path.Key, condition);
                resultTerms[resultTerm] = condition;
            }
            return resultTerms;
        }

        private void dump(UniqueSubtermCounter subterms, TextWriter writer, Term value, TypeEx type)
        {
            try
            {
                IMethodBodyWriter codeWriter = this.Services.TestManager.Language.CreateBodyWriter(
                    writer,
                    VisibilityContext.Private,
                    100);
                if (subterms != null)
                    subterms.VisitTerm(default(TVoid), value);
                if (!this.emitter.TryEvaluate(
                    new Term[] { value },
                    10000, // bound on size of expression we are going to pretty-print
                    codeWriter))
                {
                    writer.WriteLine("(expression too big; consider using environment variable {0})", ExtendedReflectionEnvironmentSettings.NoCodeEmitterSizeLimit.Name);
                    return;
                }

                codeWriter.Return(type);
            }
            catch (OutOfMemoryException)
            {
                writer.WriteLine("OutOfMemoryException");
            }
        }

        private void dumpHelper(UniqueSubtermCounter subterms, TextWriter writer, Term condition, Term value, TypeEx type)
        {
            IMethodBodyWriter codeWriter = this.Services.TestManager.Language.CreateBodyWriter(
                writer,
                VisibilityContext.Private,
                100);

            if (!this.termManager.IsTrue(condition))
            {
                if (subterms != null)
                    subterms.VisitTerm(default(TVoid), condition);
                if (!this.emitter.TryEvaluate(
                    new Term[] { condition },
                    10000, // bound on size of expression we are going to pretty-print
                    codeWriter))
                {
                    writer.WriteLine("(expression too big; consider using environment variable {0})", ExtendedReflectionEnvironmentSettings.NoCodeEmitterSizeLimit.Name);
                    return;
                }
                codeWriter.BeginIfThenElse();
                codeWriter.BeginThen();
            }

            if (subterms != null)
                subterms.VisitTerm(default(TVoid), value);
            if (!this.emitter.TryEvaluate(
                new Term[] { value },
                10000, // bound on size of expression we are going to pretty-print
                codeWriter))
            {
                writer.WriteLine("(expression too big; consider using environment variable {0})", ExtendedReflectionEnvironmentSettings.NoCodeEmitterSizeLimit.Name);
                return;
            }
            codeWriter.Return(type);

            if (!this.termManager.IsTrue(condition))
            {
                codeWriter.EndThen();
                codeWriter.EndIfThenElse();
            }
        }

        private void dump(UniqueSubtermCounter subterms, TextWriter writer, Term condition, Term value, TypeEx type)
        {
            try
            {
                dumpHelper(subterms, writer, condition, value, type);
            }
            catch (OutOfMemoryException)
            {
                writer.WriteLine("OutOfMemoryException");
            }
        }

        public void SetImpure(Method method)
        {
            this.impureMethods.Add(method.Definition);
        }
    }
}
